$\forall$$T$:(Id$\rightarrow$Id$\rightarrow$Type$_{\mbox{\scriptsize i}}$), $V$:(Id$\rightarrow$Knd$\rightarrow$Type$_{\mbox{\scriptsize i}}$). ESAtomAxiom\{i:l\}($T$; $V$) $\in$ Prop$_{\mbox{\scriptsize i'}}$